i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da),
upd:update-spec(ds;da).
update-spec-decl(upd;ds)
 "ecl"  dom(ds)
 ecl-machine at i with state eclAstate variables dsactions dasends sndupdates upd  Realizer 

latex

Definitions

t  T, "$x", Id, P  Q, x:A. B(x), ecl-machine3(ds;da;x;T;ks;a;snd), ecl-machine2(i;ds;da;x;T;ks;a;upd), left  right, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), x:AB(x), ecl-trans-tuple{i:l}(ds;da), ecl-trans(x), x:AB(x), s = t, ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, Type, x. t(x), a:A fp B(a), Knd, ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), update-spec-decl(upd;ds), x.A(x), Top, IdDeq, x  dom(f), b, A, Realizer

Lemmas

not wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, update-spec-decl wf, update-spec wf, msg-spec wf, ecl wf, Knd wf, fpf wf, Id wf, ecl-machine1 wf, ecl-trans wf, ecl-trans-tuple wf, Rplus wf, ecl-machine2 wf, ecl-machine3 wf